FDL - Step of Proof: fun_exp

Step of Proof: fun_exp_add-sq

11,40

Inference at * 1 1
Iof proof for Lemma fun exp add-sq:

1. n :

2. 0 < n
3.

, f, x:Top.
3. (primrec((n - 1)+m;

x.x;

i,g. f o g)(x))
3. ~
3. (primrec(n - 1;

x.x;

i,g. f o g)(primrec(m;

x.x;

i,g. f o g)(x)))
4. m :

5. f : Top
6. x : Top
7.

(n = 0)
8.

(n+m = 0)

(primrec((n+m) - 1;

x.x;

i,g. f o g)(x))

(primrec(n - 1;

x.x;

i,g. f o g)(primrec(m;

x.x;

i,g. f o g)(x)))

by ((((RW (SweepDnC (RevHypC 3)) 0)
CollapseTHENA (Auto

))

)
CCollapseTHEN ((((if (((first_nat
CC2:n)) = 0) then (Repeat (((EqCD)
CCollapseTHEN ((Try (Trivial))

))

)) else (RepeatFor (first_nat
CC2:n) (((EqCD)
CCollapseTHEN ((Try (Trivial))

))

)))

)
CCollapseTHEN (Auto'))

))

CC.

Definitions primrec(n;b;c), x.A(x), f o g, f(a), {x:A| B(x)} , s ~ t, #$n, A, Top, , x:A. B(x), x:AB(x), a < b, , s = t, n+m, t T, n - m